(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun k () Int)
(declare-fun l () Int)
(declare-fun m () Int)
(declare-fun n () Int)
(declare-fun o () Int)
(declare-fun p () Int)
(assert (or (and (>= m 0) (> (* i d) 0) (= (mod 1 c) 0) (>= c 0) (>= d 0) (= (+ (- m) a (* e d)) (+ c (* f d)) 0))))
(assert (<= (+ (* a o) j) 0 (+ i (* e o) (* f j)) 0))
(assert (or (and (>= g 0 p l (* h k) 0) (= (+ g (* a k) (+ e l)) (+ (- 1) k (* f l)) (+ g (* b k) 2 (* n k)) 0))))
(check-sat)
